/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sofia Rodrigues
-/
module

prelude
public import Std.Time
public import Std.Internal.UV.Signal
public import Std.Internal.Async.Select

public section

namespace Std
namespace Internal
namespace IO
namespace Async

/--
Unix style signals for Unix and Windows. SIGKILL and SIGSTOP are missing because they cannot be caught.
SIGPIPE is not present because the runtime ignores the signal.
-/
inductive Signal

  /--
  Hangup detected on controlling terminal or death of controlling process. SIGHUP is not
  generated when terminal raw mode is enabled.

  On Windows:
  * SIGHUP is generated when the user closes the console window. The program is given ~10 seconds to
    cleanup before Windows unconditionally terminates it.
  -/
  | sighup

  /--
  Interrupt program.

  * Normally delivered when the user presses CTRL+C. Not generated when terminal raw mode is enabled (like Unix).
  -/
  | sigint

  /--
  Quit program.
  -/
  | sigquit

  /--
  Trace/breakpoint trap.
  -/
  | sigtrap

  /--
  Abort signal.

  Notes:
  - SIGABRT is not catchable if generated by certain runtime functions, such as abort or assertion failure.
  - On Windows, watchers can be created for SIGABRT, but they never receive the signal.
  -/
  | sigabrt

  /--
  Emulate instruction executed
  -/
  | sigemt

  /--
  Bad system call.
  -/
  | sigsys

  /--
  Real-time timer expired.
  -/
  | sigalrm

  /--
  Termination signal.

  Notes:
  - On Windows, watchers can be created for SIGTERM, but they never receive the signal.
  -/
  | sigterm

  /--
  Urgent condition on socket.
  -/
  | sigurg

  /--
  Stop typed at tty.
  -/
  | sigtstp

  /--
  Continue after stop.
  -/
  | sigcont

  /--
  Child status has changed.
  -/
  | sigchld

  /--
  Background read attempted from control terminal.
  -/
  | sigttin

  /--
  Background write attempted to control terminal
  -/
  | sigttou

  /--
  I/O now possible.
  -/
  | sigio

  /--
  CPU time limit exceeded.
  -/
  | sigxcpu

  /--
  File size limit exceeded.
  -/
  | sigxfsz

  /--
  Virtual alarm clock.
  -/
  | sigvtalrm

  /--
  Profiling timer expired.
  -/
  | sigprof

  /--
  Window size change.

  Notes:
  - SIGWINCH is raised whenever the runtime detects the console has been resized.
  - Under console emulators, or on 32-bit apps on 64-bit systems, SIGWINCH is emulated.
  - In these cases, signals may not be delivered timely.
  -/
  | sigwinch

  /--
  Status request from keyboard.
  -/
  | siginfo

  /--
  User-defined signal 1.
  -/
  | sigusr1

  /--
  User-defined signal 2.
  -/
  | sigusr2

deriving Repr, DecidableEq, BEq

namespace Signal

/--
Converts a `Signal` to its corresponding `Int32` value as defined in the libc `signal.h`.
-/
def toInt32 : Signal → Int32
  | .sighup => 1
  | .sigint => 2
  | .sigquit => 3
  | .sigtrap => 5
  | .sigabrt => 6
  | .sigemt => 7
  | .sigsys => 12
  | .sigalrm => 14
  | .sigterm => 15
  | .sigurg => 16
  | .sigtstp => 18
  | .sigcont => 19
  | .sigchld => 20
  | .sigttin => 21
  | .sigttou => 22
  | .sigio => 23
  | .sigxcpu => 24
  | .sigxfsz => 25
  | .sigvtalrm => 26
  | .sigprof => 27
  | .sigwinch => 28
  | .siginfo => 29
  | .sigusr1 => 30
  | .sigusr2 => 31

/--
`Signal.Waiter` can be used to handle a specific signal once.
-/
structure Waiter where
  private ofNative ::
    native : Internal.UV.Signal

namespace Waiter

/--
Set up a `Signal.Waiter` that waits for the specified `signum`.
This function only initializes but does not yet start listening for the signal.
-/
@[inline]
def mk (signum : Signal) (repeating : Bool) : IO Signal.Waiter := do
  let native ← Internal.UV.Signal.mk signum.toInt32 repeating
  return .ofNative native

/--
If:
- `s` is not yet running start listening and return an `AsyncTask` that will resolve once the
   previously configured signal is received.
- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`.

The resolved `AsyncTask` contains the signal number that was received.
-/
@[inline]
def wait (s : Signal.Waiter) : IO (AsyncTask Int) := do
  let promise ← s.native.next
  return .ofPurePromise promise

/--
If:
- `s` is still running this stops `s` without resolving any remaining `AsyncTask`s that were created
  through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang
  forever without further intervention.
- `s` is not yet or not anymore running this is a no-op.
-/
@[inline]
def stop (s : Signal.Waiter) : IO Unit :=
  s.native.stop

/--
Create a `Selector` that resolves once `s` has received the signal. Note that calling this function
does not start the signal waiter.
-/
def selector (s : Signal.Waiter) : Selector Unit :=
  {
    tryFn := do
      let signalWaiter : AsyncTask _ ← async s.wait
      if ← IO.hasFinished signalWaiter then
        return some ()
      else
        s.native.cancel
        return none

    registerFn waiter := do
      let signalWaiter ← s.wait
      discard <| AsyncTask.mapIO (x := signalWaiter) fun _ => do
        let lose := return ()
        let win promise := promise.resolve (.ok ())
        waiter.race lose win

    unregisterFn := s.native.cancel

  }
